$\forall$${\it es}$:ES, ${\it e'}$:E, $P$:(\{$e$:E$\mid$ loc($e$) $=$ loc(${\it e'}$) $\in$ Id \}$\rightarrow$Prop).
\\[0ex]$\forall$$e$@loc(${\it e'}$). Dec($P$($e$)) $\Rightarrow$ ($\exists$$e$$<$${\it e'}$.$e$ is first@ loc(${\it e'}$) s.t.  $e$.$P$($e$) $\Leftrightarrow$ $\exists$$e$$<$${\it e'}$.$P$($e$))